0 QTRS
↳1 QTRSRRRProof (⇔)
↳2 QTRS
↳3 QTRSRRRProof (⇔)
↳4 QTRS
↳5 QTRSRRRProof (⇔)
↳6 QTRS
↳7 QTRSRRRProof (⇔)
↳8 QTRS
↳9 QTRSRRRProof (⇔)
↳10 QTRS
↳11 Overlay + Local Confluence (⇔)
↳12 QTRS
↳13 DependencyPairsProof (⇔)
↳14 QDP
↳15 DependencyGraphProof (⇔)
↳16 AND
↳17 QDP
↳18 UsableRulesProof (⇔)
↳19 QDP
↳20 QReductionProof (⇔)
↳21 QDP
↳22 QDPSizeChangeProof (⇔)
↳23 YES
↳24 QDP
↳25 UsableRulesProof (⇔)
↳26 QDP
↳27 QReductionProof (⇔)
↳28 QDP
↳29 UsableRulesReductionPairsProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Narrowing (⇔)
↳34 QDP
↳35 UsableRulesProof (⇔)
↳36 QDP
↳37 QReductionProof (⇔)
↳38 QDP
↳39 Rewriting (⇔)
↳40 QDP
↳41 UsableRulesProof (⇔)
↳42 QDP
↳43 QReductionProof (⇔)
↳44 QDP
↳45 Instantiation (⇔)
↳46 QDP
↳47 NonTerminationProof (⇔)
↳48 NO
zeros → cons(0, n__zeros)
and(tt, X) → activate(X)
length(nil) → 0
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = x1
POL(and(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = x1
POL(n__take(x1, x2)) = x1 + 2·x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x1 + 2·x2
POL(tt) = 2
POL(zeros) = 0
and(tt, X) → activate(X)
zeros → cons(0, n__zeros)
length(nil) → 0
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = x1
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = 1 + 2·x1
POL(n__take(x1, x2)) = 2·x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 2·x1 + x2
POL(zeros) = 0
length(nil) → 0
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = 2·x1
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(length(x1)) = 2·x1
POL(n__take(x1, x2)) = 1 + x1 + x2
POL(n__zeros) = 0
POL(nil) = 2
POL(s(x1)) = x1
POL(take(x1, x2)) = 2 + 2·x1 + 2·x2
POL(zeros) = 0
take(X1, X2) → n__take(X1, X2)
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = 2·x1
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(length(x1)) = x1
POL(n__take(x1, x2)) = 1 + x1 + x2
POL(n__zeros) = 0
POL(nil) = 1
POL(s(x1)) = x1
POL(take(x1, x2)) = 2 + 2·x1 + 2·x2
POL(zeros) = 0
take(0, IL) → nil
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = 1 + 2·x1
POL(cons(x1, x2)) = 1 + 2·x1 + 2·x2
POL(length(x1)) = x1
POL(n__take(x1, x2)) = x1 + x2
POL(n__zeros) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + 2·x1 + 2·x2
POL(zeros) = 1
zeros → n__zeros
activate(X) → X
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
zeros
length(cons(x0, x1))
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
LENGTH(cons(N, L)) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
zeros
length(cons(x0, x1))
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
zeros
length(cons(x0, x1))
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
zeros
length(cons(x0, x1))
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
zeros
length(cons(x0, x1))
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
From the DPs we obtained the following set of size-change graphs:
LENGTH(cons(N, L)) → LENGTH(activate(L))
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
zeros
length(cons(x0, x1))
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
LENGTH(cons(N, L)) → LENGTH(activate(L))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → cons(0, n__zeros)
zeros
length(cons(x0, x1))
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
length(cons(x0, x1))
LENGTH(cons(N, L)) → LENGTH(activate(L))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → cons(0, n__zeros)
zeros
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
Used ordering: POLO with Polynomial interpretation [POLO]:
activate(n__take(X1, X2)) → take(X1, X2)
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
POL(0) = 0
POL(LENGTH(x1)) = x1
POL(activate(x1)) = x1
POL(cons(x1, x2)) = x1 + 2·x2
POL(n__take(x1, x2)) = 1 + 2·x1 + x2
POL(n__zeros) = 0
POL(s(x1)) = 2 + 2·x1
POL(take(x1, x2)) = 2·x1 + x2
POL(zeros) = 0
LENGTH(cons(N, L)) → LENGTH(activate(L))
activate(n__zeros) → zeros
zeros → cons(0, n__zeros)
zeros
take(s(x0), cons(x1, x2))
activate(n__zeros)
activate(n__take(x0, x1))
take(s(x0), cons(x1, x2))
LENGTH(cons(N, L)) → LENGTH(activate(L))
activate(n__zeros) → zeros
zeros → cons(0, n__zeros)
zeros
activate(n__zeros)
activate(n__take(x0, x1))
LENGTH(cons(y0, n__zeros)) → LENGTH(zeros)
LENGTH(cons(y0, n__zeros)) → LENGTH(zeros)
activate(n__zeros) → zeros
zeros → cons(0, n__zeros)
zeros
activate(n__zeros)
activate(n__take(x0, x1))
LENGTH(cons(y0, n__zeros)) → LENGTH(zeros)
zeros → cons(0, n__zeros)
zeros
activate(n__zeros)
activate(n__take(x0, x1))
activate(n__zeros)
activate(n__take(x0, x1))
LENGTH(cons(y0, n__zeros)) → LENGTH(zeros)
zeros → cons(0, n__zeros)
zeros
LENGTH(cons(y0, n__zeros)) → LENGTH(cons(0, n__zeros))
LENGTH(cons(y0, n__zeros)) → LENGTH(cons(0, n__zeros))
zeros → cons(0, n__zeros)
zeros
LENGTH(cons(y0, n__zeros)) → LENGTH(cons(0, n__zeros))
zeros
zeros
LENGTH(cons(y0, n__zeros)) → LENGTH(cons(0, n__zeros))
LENGTH(cons(0, n__zeros)) → LENGTH(cons(0, n__zeros))
LENGTH(cons(0, n__zeros)) → LENGTH(cons(0, n__zeros))